r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
e(r(x)) → r(w(x))
t(i(x)) → r(e(x))
w(e(x)) → i(r(x))
e(t(x)) → e(r(x))
r(w(x)) → t(i(x))
r(e(x)) → w(e(x))
r(e(t(i(r(x))))) → e(t(i(r(w(e(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS
↳ QTRS Reverse
↳ DependencyPairsProof
e(r(x)) → r(w(x))
t(i(x)) → r(e(x))
w(e(x)) → i(r(x))
e(t(x)) → e(r(x))
r(w(x)) → t(i(x))
r(e(x)) → w(e(x))
r(e(t(i(r(x))))) → e(t(i(r(w(e(x))))))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
e(r(x)) → r(w(x))
t(i(x)) → r(e(x))
w(e(x)) → i(r(x))
e(t(x)) → e(r(x))
r(w(x)) → t(i(x))
r(e(x)) → w(e(x))
r(e(t(i(r(x))))) → e(t(i(r(w(e(x))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ QTRS
↳ DependencyPairsProof
e(r(x)) → r(w(x))
t(i(x)) → r(e(x))
w(e(x)) → i(r(x))
e(t(x)) → e(r(x))
r(w(x)) → t(i(x))
r(e(x)) → w(e(x))
r(e(t(i(r(x))))) → e(t(i(r(w(e(x))))))
E(w(x1)) → R(i(x1))
E(r(x1)) → W(x1)
R(i(t(e(r(x1))))) → W(r(i(t(e(x1)))))
R(i(t(e(r(x1))))) → I(t(e(x1)))
R(e(x1)) → W(r(x1))
W(r(x1)) → T(x1)
E(w(x1)) → I(x1)
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
I(t(x1)) → R(x1)
R(i(t(e(r(x1))))) → T(e(x1))
W(r(x1)) → I(t(x1))
I(t(x1)) → E(r(x1))
R(e(x1)) → R(x1)
R(i(t(e(r(x1))))) → R(i(t(e(x1))))
R(i(t(e(r(x1))))) → E(x1)
E(r(x1)) → E(w(x1))
T(e(x1)) → R(e(x1))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
E(w(x1)) → R(i(x1))
E(r(x1)) → W(x1)
R(i(t(e(r(x1))))) → W(r(i(t(e(x1)))))
R(i(t(e(r(x1))))) → I(t(e(x1)))
R(e(x1)) → W(r(x1))
W(r(x1)) → T(x1)
E(w(x1)) → I(x1)
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
I(t(x1)) → R(x1)
R(i(t(e(r(x1))))) → T(e(x1))
W(r(x1)) → I(t(x1))
I(t(x1)) → E(r(x1))
R(e(x1)) → R(x1)
R(i(t(e(r(x1))))) → R(i(t(e(x1))))
R(i(t(e(r(x1))))) → E(x1)
E(r(x1)) → E(w(x1))
T(e(x1)) → R(e(x1))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
E(w(x1)) → I(x1)
Used ordering: Polynomial Order [21,25] with Interpretation:
E(w(x1)) → R(i(x1))
E(r(x1)) → W(x1)
R(i(t(e(r(x1))))) → W(r(i(t(e(x1)))))
R(i(t(e(r(x1))))) → I(t(e(x1)))
R(e(x1)) → W(r(x1))
W(r(x1)) → T(x1)
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
I(t(x1)) → R(x1)
R(i(t(e(r(x1))))) → T(e(x1))
W(r(x1)) → I(t(x1))
I(t(x1)) → E(r(x1))
R(e(x1)) → R(x1)
R(i(t(e(r(x1))))) → R(i(t(e(x1))))
R(i(t(e(r(x1))))) → E(x1)
E(r(x1)) → E(w(x1))
T(e(x1)) → R(e(x1))
POL( E(x1) ) = x1 + 1
POL( i(x1) ) = max{0, x1 - 1}
POL( T(x1) ) = x1 + 1
POL( w(x1) ) = x1
POL( t(x1) ) = x1 + 1
POL( e(x1) ) = x1
POL( r(x1) ) = x1
POL( R(x1) ) = x1 + 1
POL( I(x1) ) = x1
POL( W(x1) ) = x1 + 1
e(r(x1)) → e(w(x1))
e(w(x1)) → r(i(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
i(t(x1)) → e(r(x1))
r(e(x1)) → w(r(x1))
w(r(x1)) → i(t(x1))
t(e(x1)) → r(e(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
E(w(x1)) → R(i(x1))
E(r(x1)) → W(x1)
R(i(t(e(r(x1))))) → W(r(i(t(e(x1)))))
R(i(t(e(r(x1))))) → I(t(e(x1)))
R(e(x1)) → W(r(x1))
W(r(x1)) → T(x1)
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
I(t(x1)) → R(x1)
R(i(t(e(r(x1))))) → T(e(x1))
W(r(x1)) → I(t(x1))
I(t(x1)) → E(r(x1))
R(e(x1)) → R(x1)
R(i(t(e(r(x1))))) → R(i(t(e(x1))))
R(i(t(e(r(x1))))) → E(x1)
E(r(x1)) → E(w(x1))
T(e(x1)) → R(e(x1))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
E(r(x1)) → W(x1)
R(i(t(e(r(x1))))) → W(r(i(t(e(x1)))))
R(i(t(e(r(x1))))) → I(t(e(x1)))
W(r(x1)) → T(x1)
I(t(x1)) → R(x1)
R(i(t(e(r(x1))))) → T(e(x1))
R(e(x1)) → R(x1)
R(i(t(e(r(x1))))) → R(i(t(e(x1))))
R(i(t(e(r(x1))))) → E(x1)
E(r(x1)) → E(w(x1))
Used ordering: Polynomial interpretation [25]:
E(w(x1)) → R(i(x1))
R(e(x1)) → W(r(x1))
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
W(r(x1)) → I(t(x1))
I(t(x1)) → E(r(x1))
T(e(x1)) → R(e(x1))
POL(E(x1)) = 1 + 2·x1
POL(I(x1)) = x1
POL(R(x1)) = 3 + 4·x1
POL(T(x1)) = 3 + 4·x1
POL(W(x1)) = 1 + 2·x1
POL(e(x1)) = 1 + 2·x1
POL(i(x1)) = x1
POL(r(x1)) = 3 + 4·x1
POL(t(x1)) = 7 + 8·x1
POL(w(x1)) = 1 + 2·x1
e(r(x1)) → e(w(x1))
e(w(x1)) → r(i(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
i(t(x1)) → e(r(x1))
r(e(x1)) → w(r(x1))
w(r(x1)) → i(t(x1))
t(e(x1)) → r(e(x1))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
I(t(x1)) → E(r(x1))
E(w(x1)) → R(i(x1))
R(e(x1)) → W(r(x1))
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
T(e(x1)) → R(e(x1))
W(r(x1)) → I(t(x1))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
E(w(x1)) → R(i(x1))
I(t(x1)) → E(r(x1))
R(e(x1)) → W(r(x1))
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
W(r(x1)) → I(t(x1))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
I(t(i(t(e(r(x0)))))) → E(e(w(r(i(t(e(x0)))))))
I(t(e(x0))) → E(w(r(x0)))
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ SemLabProof
E(w(x1)) → R(i(x1))
R(e(x1)) → W(r(x1))
R(i(t(e(r(x1))))) → E(w(r(i(t(e(x1))))))
I(t(i(t(e(r(x0)))))) → E(e(w(r(i(t(e(x0)))))))
W(r(x1)) → I(t(x1))
I(t(e(x0))) → E(w(r(x0)))
r(e(x1)) → w(r(x1))
i(t(x1)) → e(r(x1))
e(w(x1)) → r(i(x1))
t(e(x1)) → r(e(x1))
w(r(x1)) → i(t(x1))
e(r(x1)) → e(w(x1))
r(i(t(e(r(x1))))) → e(w(r(i(t(e(x1))))))
I.1(t.0(i.1(t.0(e.0(r.1(x0)))))) → E.0(e.0(w.0(r.0(i.1(t.0(e.1(x0)))))))
E.0(w.0(x1)) → R.0(i.0(x1))
W.0(r.1(x1)) → I.1(t.1(x1))
R.0(e.1(x1)) → W.0(r.1(x1))
I.1(t.0(e.0(x0))) → E.0(w.0(r.0(x0)))
I.1(t.0(i.1(t.0(e.0(r.0(x0)))))) → E.0(e.0(w.0(r.0(i.1(t.0(e.0(x0)))))))
W.0(r.0(x1)) → I.1(t.0(x1))
W.0(r.1(x1)) → I.0(t.1(x1))
E.0(w.1(x1)) → R.0(i.1(x1))
W.0(r.0(x1)) → I.0(t.0(x1))
R.0(i.1(t.0(e.0(r.0(x1))))) → E.0(w.0(r.0(i.1(t.0(e.0(x1))))))
I.1(t.0(e.1(x0))) → E.0(w.0(r.1(x0)))
R.0(e.0(x1)) → W.0(r.0(x1))
R.0(i.1(t.0(e.0(r.1(x1))))) → E.0(w.0(r.0(i.1(t.0(e.1(x1))))))
r.0(e.0(x1)) → w.0(r.0(x1))
e.0(w.1(x1)) → r.0(i.1(x1))
t.0(e.0(x1)) → r.0(e.0(x1))
t.1(x0) → t.0(x0)
r.0(e.1(x1)) → w.0(r.1(x1))
e.0(r.1(x1)) → e.0(w.1(x1))
w.1(x0) → w.0(x0)
r.0(i.1(t.0(e.0(r.1(x1))))) → e.0(w.0(r.0(i.1(t.0(e.1(x1))))))
e.0(w.0(x1)) → r.0(i.0(x1))
w.0(r.0(x1)) → i.1(t.0(x1))
r.1(x0) → r.0(x0)
i.1(t.1(x1)) → e.0(r.1(x1))
e.0(r.0(x1)) → e.0(w.0(x1))
i.1(t.0(x1)) → e.0(r.0(x1))
t.0(e.1(x1)) → r.0(e.1(x1))
w.0(r.1(x1)) → i.1(t.1(x1))
e.1(x0) → e.0(x0)
r.0(i.1(t.0(e.0(r.0(x1))))) → e.0(w.0(r.0(i.1(t.0(e.0(x1))))))
i.1(x0) → i.0(x0)
↳ QTRS
↳ QTRS Reverse
↳ QTRS Reverse
↳ DependencyPairsProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ DependencyGraphProof
↳ QDP
↳ Narrowing
↳ QDP
↳ SemLabProof
↳ QDP
↳ DependencyGraphProof
I.1(t.0(i.1(t.0(e.0(r.1(x0)))))) → E.0(e.0(w.0(r.0(i.1(t.0(e.1(x0)))))))
E.0(w.0(x1)) → R.0(i.0(x1))
W.0(r.1(x1)) → I.1(t.1(x1))
R.0(e.1(x1)) → W.0(r.1(x1))
I.1(t.0(e.0(x0))) → E.0(w.0(r.0(x0)))
I.1(t.0(i.1(t.0(e.0(r.0(x0)))))) → E.0(e.0(w.0(r.0(i.1(t.0(e.0(x0)))))))
W.0(r.0(x1)) → I.1(t.0(x1))
W.0(r.1(x1)) → I.0(t.1(x1))
E.0(w.1(x1)) → R.0(i.1(x1))
W.0(r.0(x1)) → I.0(t.0(x1))
R.0(i.1(t.0(e.0(r.0(x1))))) → E.0(w.0(r.0(i.1(t.0(e.0(x1))))))
I.1(t.0(e.1(x0))) → E.0(w.0(r.1(x0)))
R.0(e.0(x1)) → W.0(r.0(x1))
R.0(i.1(t.0(e.0(r.1(x1))))) → E.0(w.0(r.0(i.1(t.0(e.1(x1))))))
r.0(e.0(x1)) → w.0(r.0(x1))
e.0(w.1(x1)) → r.0(i.1(x1))
t.0(e.0(x1)) → r.0(e.0(x1))
t.1(x0) → t.0(x0)
r.0(e.1(x1)) → w.0(r.1(x1))
e.0(r.1(x1)) → e.0(w.1(x1))
w.1(x0) → w.0(x0)
r.0(i.1(t.0(e.0(r.1(x1))))) → e.0(w.0(r.0(i.1(t.0(e.1(x1))))))
e.0(w.0(x1)) → r.0(i.0(x1))
w.0(r.0(x1)) → i.1(t.0(x1))
r.1(x0) → r.0(x0)
i.1(t.1(x1)) → e.0(r.1(x1))
e.0(r.0(x1)) → e.0(w.0(x1))
i.1(t.0(x1)) → e.0(r.0(x1))
t.0(e.1(x1)) → r.0(e.1(x1))
w.0(r.1(x1)) → i.1(t.1(x1))
e.1(x0) → e.0(x0)
r.0(i.1(t.0(e.0(r.0(x1))))) → e.0(w.0(r.0(i.1(t.0(e.0(x1))))))
i.1(x0) → i.0(x0)